basic
monot(T;x,y.R(x;y);f) == x, y:T. R(x;y)  R(f(x);f(y)) 

latex

---

clarification:

basic
monot(T;x,y.R(x;y);f) == x:T, y:T. R(x;y)  R(f(x);f(y)) 

latex

Up	gen algebra 1
Wellformedness Lemmas	monot wf
Definitions	x:A. B(x), P  Q